\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), ${\it snd}$:msg{-}spec(${\it ds}$; ${\it da}$), ${\it upd}$:update{-}spec(\=${\it ds}$;\+\+
\\[0ex]${\it da}$),
\-\\[0ex]$T$:Type, ${\it ks}$:(Knd List), $a$:($\mathbb{N}\rightarrow$(\=$k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}$)\} $\rightarrow$decl{-}state(${\it ds}$)$\rightarrow$ma{-}valtype(${\it da}$; $k$)$\rightarrow$$T$\+
\\[0ex]$\rightarrow\mathbb{B}$)),
\-\\[0ex]$x$:Id.
\-\\[0ex]($\neg$($\uparrow$fpf{-}dom(id{-}deq; $x$; ${\it ds}$)))
\\[0ex]$\Rightarrow$ update{-}spec{-}decl(${\it upd}$; ${\it ds}$)
\\[0ex]$\Rightarrow$ ($\forall$$k$:Knd. ($k$ $\in$ ${\it ks}$) $\Rightarrow$ ($\uparrow$fpf{-}dom(Kind{-}deq; $k$; ${\it da}$)))
\\[0ex]$\Rightarrow$ R{-}compat\=\{i:l\}\+
\\[0ex](\=ecl{-}machine2($i$; ${\it ds}$; ${\it da}$; $x$; $T$; ${\it ks}$; $a$; ${\it upd}$);\+
\\[0ex]ecl{-}machine3(${\it ds}$; ${\it da}$; $x$; $T$; ${\it ks}$; $a$; ${\it snd}$))
\-\-
\end{tabbing}